package sketch.specs;

import java.io.File;
import java.io.IOException;
import java.util.LinkedHashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Set;

import org.eclipse.jdt.core.dom.MethodDeclaration;
import org.eclipse.jdt.core.dom.PackageDeclaration;
import org.eclipse.jdt.core.dom.TypeDeclaration;

import randoop.util.Files;
import sketch.ast.ASTUtils;
import sketch.util.Checker;
import sketch.util.Globals;

public class WriteJPFSymbolicTestDriver {
	
	//should also add imports
	public static List<File> writeTestDriver(PackageDeclaration package_decl, TypeDeclaration type, String dir, String[] methodsUnderTest, String packageName,
			String[] extraDependentClasses) {
		return writeTestDriver(package_decl, type, dir, methodsUnderTest, packageName,
				extraDependentClasses, false, false);
	}
	
	public static List<File> writeTestDriver(PackageDeclaration package_decl, TypeDeclaration type, String dir, String[] methodsUnderTest, String packageName,
			String[] extraDependentClasses, boolean hasSetUp, boolean hasTearDown) {
		List<File> driverFiles = new LinkedList<File>();
		
		MethodDeclaration[] declarations = type.getMethods();
		Set<String> methodSet = new LinkedHashSet<String>();
		for(String methodUnderTest : methodsUnderTest) {
			methodSet.add(methodUnderTest);
		}
		//process every method
		for(MethodDeclaration declaration : declarations) {
			String methodName = declaration.getName().getIdentifier();
			if(!methodSet.contains(methodName)) {
				continue;
			}
			//check the modifiers
			Checker.checkTrue(declaration.parameters().isEmpty(), "The parameter of method: " + methodName + " is not empty!");
			Checker.checkTrue(ASTUtils.isPublic(declaration), "The given method should be public!");
			Checker.checkTrue(declaration.getReturnType2().toString().equals("void"), "The return type of method: " + methodName + " is not void.");
			
			String singleDriverName = type.getName().getIdentifier() + "_" + methodName;
			String singleFilePath = dir + Globals.fileSep +  singleDriverName + ".java";
			File file = writeSingleDriver(singleFilePath, packageName, singleDriverName, (package_decl == null ? null : package_decl.getName().toString()),
					type.getName().getIdentifier(), methodName, extraDependentClasses, hasSetUp, hasTearDown);
			driverFiles.add(file);
		}
		
		return driverFiles;
		
	}
	
	private static File writeSingleDriver(String filePath, String packageName, String driverName, String testClassPackageName,
			String testClassName, String methodName, String[] extraDependentClasses, boolean hasSetUp, boolean hasTearDown) {
		File file = new File(filePath);
		StringBuilder sb = new StringBuilder();
		
		//set the file content
		if(packageName != null && !packageName.equals("")) {
		  sb.append("package " + packageName + ";");
		  sb.append(Globals.lineSep);
		}
		
		if(extraDependentClasses != null) {
		  for(String extraImport : extraDependentClasses) {
			sb.append("import " + extraImport + ";");
			sb.append(Globals.lineSep);
		  }
		}
		
		sb.append("import gov.nasa.jpf.symbc.Debug;");
		sb.append(Globals.lineSep);
		
		sb.append("public class " + driverName + " {");
		sb.append(Globals.lineSep);
		sb.append("  public static void main(String[] args) {" + Globals.lineSep);
		sb.append("    " + (testClassPackageName == null ? "" : testClassPackageName + ".") + testClassName
				+ " c = new " + (testClassPackageName == null ? "" : testClassPackageName + ".") + testClassName
				+ "();" + Globals.lineSep);
		if(hasSetUp) {
			sb.append("    c.setUp(); " + Globals.lineSep);
		}
		sb.append("    c." + methodName + "();" + Globals.lineSep);
		if(hasTearDown) {
			sb.append("    c.tearDown();" + Globals.lineSep);
		}
//		sb.append("    Debug.printPC(\"" + driverName + " Path Condition: \");" + Globals.lineSep);
		sb.append("    Debug.getSolvedPC();" + Globals.lineSep);
		sb.append("  }" + Globals.lineSep);
		sb.append("}" + Globals.lineSep);
		
		//write to the file
		try {
			Files.writeToFile(sb.toString(), file);
			return file;
		} catch (IOException e) {
			throw new RuntimeException(e);
		}
	}
	
	private static File writeSingleDriver(String filePath, String packageName, String driverName, String testClassPackageName,
			String testClassName, String methodName, String[] extraDependentClasses) {
		return writeSingleDriver(filePath, packageName, driverName, testClassPackageName,
				testClassName, methodName, extraDependentClasses, false, false);
	}
	
}